Disunification in ACI 1 Theories
Identifieur interne : 006C16 ( Main/Exploration ); précédent : 006C15; suivant : 006C17Disunification in ACI 1 Theories
Auteurs : Agostino Dovier [Italie] ; Carla Piazza [Italie] ; Enrico Pontelli [États-Unis]Source :
- Constraints [ 1383-7133 ] ; 2004-01-01.
English descriptors
- KwdEn :
Abstract
Abstract: Disunification is the problem of deciding satisfiability of a system of equations and disequations with respect to a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. This problem is of great importance, for instance, for the development of constraint solvers over sets. Its solution opens new possibilities for developing automatic tools for static analysis and software verification. In this work we provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints to manageable solved forms. We propose four solved forms, each offering an increasingly more precise description of the set of solutions. For each solved form we provide the corresponding rewriting algorithm and we study the time complexity of the transformation. Remarkably, two of the solved forms can be computed and tested in polynomial time. All these solved forms are adequate to be used in the context of a Constraint Logic Programming system—e.g., they do not introduce universal quantifications, as instead happens in some of the existing solved forms for disunification problems.
Url:
DOI: 10.1023/B:CONS.0000006182.84033.6e
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000504
- to stream Istex, to step Curation: 000500
- to stream Istex, to step Checkpoint: 001825
- to stream Main, to step Merge: 006F20
- to stream Main, to step Curation: 006C16
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Disunification in ACI 1 Theories</title><author><name sortKey="Dovier, Agostino" sort="Dovier, Agostino" uniqKey="Dovier A" first="Agostino" last="Dovier">Agostino Dovier</name></author><author><name sortKey="Piazza, Carla" sort="Piazza, Carla" uniqKey="Piazza C" first="Carla" last="Piazza">Carla Piazza</name></author><author><name sortKey="Pontelli, Enrico" sort="Pontelli, Enrico" uniqKey="Pontelli E" first="Enrico" last="Pontelli">Enrico Pontelli</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:16B59A06E3D54EB8851C6CB20479CBBCB9857F14</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1023/B:CONS.0000006182.84033.6e</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-DZ639STB-L/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000504</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000504</idno><idno type="wicri:Area/Istex/Curation">000500</idno><idno type="wicri:Area/Istex/Checkpoint">001825</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001825</idno><idno type="wicri:doubleKey">1383-7133:2004:Dovier A:disunification:in:aci</idno><idno type="wicri:Area/Main/Merge">006F20</idno><idno type="wicri:Area/Main/Curation">006C16</idno><idno type="wicri:Area/Main/Exploration">006C16</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Disunification in ACI 1 Theories</title><author><name sortKey="Dovier, Agostino" sort="Dovier, Agostino" uniqKey="Dovier A" first="Agostino" last="Dovier">Agostino Dovier</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>Dip. di Matematica e Informatica, Università di Udine, Via Le Scienze 206, 33100, Udine (</wicri:regionArea><wicri:noRegion>Udine (</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Piazza, Carla" sort="Piazza, Carla" uniqKey="Piazza C" first="Carla" last="Piazza">Carla Piazza</name><affiliation wicri:level="1"><country xml:lang="fr">Italie</country><wicri:regionArea>Dip. di Matematica e Informatica, Università di Udine, Via Le Scienze 206, 33100, Udine (</wicri:regionArea><wicri:noRegion>Udine (</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Italie</country></affiliation></author><author><name sortKey="Pontelli, Enrico" sort="Pontelli, Enrico" uniqKey="Pontelli E" first="Enrico" last="Pontelli">Enrico Pontelli</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Dept. CS, New Mexico State University, Dept. Computer Science, Box 30001, 88003 (, Las Cruces, NM</wicri:regionArea><placeName><region type="state">Nouveau-Mexique</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Constraints</title><title level="j" type="abbrev">Constraints</title><idno type="ISSN">1383-7133</idno><idno type="eISSN">1572-9354</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Boston</pubPlace><date type="published" when="2004-01-01">2004-01-01</date><biblScope unit="volume">9</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="35">35</biblScope><biblScope unit="page" to="91">91</biblScope></imprint><idno type="ISSN">1383-7133</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1383-7133</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>ACI</term><term>CLP</term><term>complexity</term><term>disunification</term><term>equational theories</term><term>sets</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Disunification is the problem of deciding satisfiability of a system of equations and disequations with respect to a given equational theory. In this paper we study the disunification problem in the context of ACI1 equational theories. This problem is of great importance, for instance, for the development of constraint solvers over sets. Its solution opens new possibilities for developing automatic tools for static analysis and software verification. In this work we provide a characterization of the interpretation structures suitable to model the axioms in ACI1 theories. The satisfiability problem is solved using known techniques for the equality constraints and novel methodologies to transform disequation constraints to manageable solved forms. We propose four solved forms, each offering an increasingly more precise description of the set of solutions. For each solved form we provide the corresponding rewriting algorithm and we study the time complexity of the transformation. Remarkably, two of the solved forms can be computed and tested in polynomial time. All these solved forms are adequate to be used in the context of a Constraint Logic Programming system—e.g., they do not introduce universal quantifications, as instead happens in some of the existing solved forms for disunification problems.</div></front></TEI><affiliations><list><country><li>Italie</li><li>États-Unis</li></country><region><li>Nouveau-Mexique</li></region></list><tree><country name="Italie"><noRegion><name sortKey="Dovier, Agostino" sort="Dovier, Agostino" uniqKey="Dovier A" first="Agostino" last="Dovier">Agostino Dovier</name></noRegion><name sortKey="Dovier, Agostino" sort="Dovier, Agostino" uniqKey="Dovier A" first="Agostino" last="Dovier">Agostino Dovier</name><name sortKey="Piazza, Carla" sort="Piazza, Carla" uniqKey="Piazza C" first="Carla" last="Piazza">Carla Piazza</name><name sortKey="Piazza, Carla" sort="Piazza, Carla" uniqKey="Piazza C" first="Carla" last="Piazza">Carla Piazza</name></country><country name="États-Unis"><region name="Nouveau-Mexique"><name sortKey="Pontelli, Enrico" sort="Pontelli, Enrico" uniqKey="Pontelli E" first="Enrico" last="Pontelli">Enrico Pontelli</name></region><name sortKey="Pontelli, Enrico" sort="Pontelli, Enrico" uniqKey="Pontelli E" first="Enrico" last="Pontelli">Enrico Pontelli</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006C16 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006C16 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:16B59A06E3D54EB8851C6CB20479CBBCB9857F14
|texte= Disunification in ACI 1 Theories
}}
| This area was generated with Dilib version V0.6.33. |  |